Software model checkers based on under-approximations and SMT solvers arevery successful at verifying safety (i.e. reachability) properties. Theycombine two key ideas -- (a) "concreteness": a counterexample in anunder-approximation is a counterexample in the original program as well, and(b) "generalization": a proof of safety of an under-approximation, produced byan SMT solver, are generalizable to proofs of safety of the original program.In this paper, we present a combination of "automatic abstraction" with theunder-approximation-driven framework. We explore two iterative approaches forobtaining and refining abstractions -- "proof based" and "counterexample based"-- and show how they can be combined into a unified algorithm. To the best ofour knowledge, this is the first application of Proof-Based Abstraction,primarily used to verify hardware, to Software Verification. We haveimplemented a prototype of the framework using Z3, and evaluate it on manybenchmarks from the Software Verification Competition. We show experimentallythat our combination is quite effective on hard instances.
展开▼
